$\forall$$T$:Type, ${\it ll}$:($T$ List) List, $n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$concat(${\it ll}$)$\parallel$}}$.
\\[0ex]$\exists$$m$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it ll}$$\parallel$}}$.
\\[0ex]$\parallel$concat(firstn($m$;${\it ll}$))$\parallel\leq$$n$
\\[0ex]\& $n$$-\parallel$concat(firstn($m$;${\it ll}$))$\parallel<\parallel$${\it ll}$[$m$]$\parallel$
\\[0ex]\& concat(${\it ll}$)[$n$] $=$ ${\it ll}$[$m$][$n$$-\parallel$concat(firstn($m$;${\it ll}$))$\parallel$] $\in$ $T$